\begin{tabbing}
$\forall$\=$E$:Type, $V$:(Knd$\rightarrow$Id$\rightarrow$Type), ${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id)), ${\it val}$:($e$:$E$$\rightarrow$$V$(kind($e$),loc($e$))),\+
\\[0ex]$e$:$E$.
\-\\[0ex]rcv?($e$) $\Rightarrow$ rmsg(${\it info}$;${\it val}$;$e$) $\in$ Msg($\lambda$$l$,${\it tg}$. $V$(rcv($l$,${\it tg}$),destination($l$)))
\end{tabbing}